NeedOptionCopatterns.agda:14,1-6
Option --copatterns needed to enable destructor patterns
when scope checking the left-hand side bla f in the definition of f
